$\forall$$k$:$\mathbb{N}$, $P$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$$\rightarrow\mathbb{B}$).
\\[0ex](($\exists$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$. $P$($i$)) $\Leftrightarrow$ 0$<$search($k$;$P$))
\\[0ex]\& (0$<$search($k$;$P$) $\Rightarrow$ $P$(search($k$;$P$)$-$1) \& ($\forall$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$. $j$$<$search($k$;$P$)$-$1 $\Rightarrow$ $\neg$$P$($j$)))